\begin{tabbing}
d{-}feasible{-}discrete($D$;${\it discrete}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$i$:Id, $x$:Id.\+
\\[0ex]($\uparrow$(${\it discrete}$($i$,$x$)))
\\[0ex]$\Rightarrow$ \=(ma{-}init{-}const(d{-}m($D$; $i$);$x$)\+
\\[0ex]\& ($\forall$$k$:Knd, $s$:d{-}m($D$; $i$).state, $v$:d{-}m($D$; $i$).da($k$). ma{-}ef{-}const(d{-}m($D$; $i$);$k$;$x$;$s$;$v$)))
\-\-
\end{tabbing}